p:FinProbSpace, a:, n:, X:RandomVariable(p;n).
(s:({0..n}Outcome). X(s) = a)  (E(n;X) = a) 

latex

Definitions	(i = j), , t  T, x:AB(x), RandomVariable(p;n), {i..j}, Outcome, , s = t, x:A. B(x), P  Q, FinProbSpace, {x:A| B(x)} , i  j , False, A, A  B, #$n, -n, n+m, n - m, a < b, Void, null, Top, type List, P & Q, i  j < k, , ||as||, Type, S  T, suptype(S; T), f(a), , <a, b>, weighted-sum(p;F), b, b, , x:A  B(x), P  Q, Unit, left + right, rv-shift(x;X), , E(n;F), x.A(x), True, T, cons-seq(x;s)
Lemmas	cons-seq wf, squash wf, true wf, ws-constant, expectation wf, rv-shift wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, random-variable wf, le wf, length wf1, int seg wf, length wf nat, null-seq wf, p-outcome wf, ge wf, nat properties, finite-prob-space wf, rationals wf, nat wf